Search Results

Documents authored by Bojanczyk, Mikolaj


Document
Invited Talk
Orbit-Finite Sets and Their Algorithms (Invited Talk)

Authors: Mikolaj Bojanczyk

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)


Abstract
An introduction to orbit-finite sets, which are a type of sets that are infinite enough to describe interesting examples, and finite enough to have algorithms running on them. The notion of orbit-finiteness is illustrated on the example of register automata, an automaton model dealing with infinite alphabets.

Cite as

Mikolaj Bojanczyk. Orbit-Finite Sets and Their Algorithms (Invited Talk). In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.ICALP.2017.1,
  author =	{Bojanczyk, Mikolaj},
  title =	{{Orbit-Finite Sets and Their Algorithms}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{1:1--1:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.1},
  URN =		{urn:nbn:de:0030-drops-74295},
  doi =		{10.4230/LIPIcs.ICALP.2017.1},
  annote =	{Keywords: Orbit-finite sets, sets with atoms, data words, register automata}
}
Document
Emptiness of Zero Automata Is Decidable

Authors: Mikolaj Bojanczyk, Hugo Gimbert, and Edon Kelmendi

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)


Abstract
Zero automata are a probabilistic extension of parity automata on infinite trees. The satisfiability of a certain probabilistic variant of MSO, called TMSO+zero, reduces to the emptiness problem for zero automata. We introduce a variant of zero automata called nonzero automata. We prove that for every zero automaton there is an equivalent nonzero automaton of quadratic size and the emptiness problem of nonzero automata is decidable, with complexity co-NP. These results imply that TMSO+zero has decidable satisfiability.

Cite as

Mikolaj Bojanczyk, Hugo Gimbert, and Edon Kelmendi. Emptiness of Zero Automata Is Decidable. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 106:1-106:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.ICALP.2017.106,
  author =	{Bojanczyk, Mikolaj and Gimbert, Hugo and Kelmendi, Edon},
  title =	{{Emptiness of Zero Automata Is Decidable}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{106:1--106:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.106},
  URN =		{urn:nbn:de:0030-drops-74745},
  doi =		{10.4230/LIPIcs.ICALP.2017.106},
  annote =	{Keywords: tree automata, probabilistic automata, monadic second-order logic}
}
Document
Which Classes of Origin Graphs Are Generated by Transducers

Authors: Mikolaj Bojanczyk, Laure Daviaud, Bruno Guillon, and Vincent Penelle

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)


Abstract
We study various models of transducers equipped with origin information. We consider the semantics of these models as particular graphs, called origin graphs, and we characterise the families of such graphs recognised by streaming string transducers.

Cite as

Mikolaj Bojanczyk, Laure Daviaud, Bruno Guillon, and Vincent Penelle. Which Classes of Origin Graphs Are Generated by Transducers. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 114:1-114:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.ICALP.2017.114,
  author =	{Bojanczyk, Mikolaj and Daviaud, Laure and Guillon, Bruno and Penelle, Vincent},
  title =	{{Which Classes of Origin Graphs Are Generated by Transducers}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{114:1--114:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.114},
  URN =		{urn:nbn:de:0030-drops-73984},
  doi =		{10.4230/LIPIcs.ICALP.2017.114},
  annote =	{Keywords: Streaming String Transducers, Origin Semantics, String-to-String Transductions, MSO Definability}
}
Document
Optimizing Tree Decompositions in MSO

Authors: Mikolaj Bojanczyk and Michal Pilipczuk

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)


Abstract
The classic algorithm of Bodlaender and Kloks solves the following problem in linear fixed-parameter time: given a tree decomposition of a graph of (possibly suboptimal) width k, compute an optimum-width tree decomposition of the graph. In this work, we prove that this problem can also be solved in MSO in the following sense: for every positive integer k, there is an MSO transduction from tree decompositions of width k to tree decompositions of optimum width. Together with our recent results, this implies that for every k there exists an MSO transduction which inputs a graph of treewidth k, and nondeterministically outputs its tree decomposition of optimum width.

Cite as

Mikolaj Bojanczyk and Michal Pilipczuk. Optimizing Tree Decompositions in MSO. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 15:1-15:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2017.15,
  author =	{Bojanczyk, Mikolaj and Pilipczuk, Michal},
  title =	{{Optimizing Tree Decompositions in MSO}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{15:1--15:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.15},
  URN =		{urn:nbn:de:0030-drops-70173},
  doi =		{10.4230/LIPIcs.STACS.2017.15},
  annote =	{Keywords: tree decomposition, treewidth, transduction, monadic second-order logic}
}
Document
Thin MSO with a Probabilistic Path Quantifier

Authors: Mikolaj Bojanczyk

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
This paper is about a variant of MSO on infinite trees where: - there is a quantifier "zero probability of choosing a path pi in 2^{omega} which makes omega(pi) true"; - the monadic quantifiers range over sets with countable topological closure. We introduce an automaton model, and show that it captures the logic.

Cite as

Mikolaj Bojanczyk. Thin MSO with a Probabilistic Path Quantifier. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 96:1-96:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.ICALP.2016.96,
  author =	{Bojanczyk, Mikolaj},
  title =	{{Thin MSO with a Probabilistic Path Quantifier}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{96:1--96:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.96},
  URN =		{urn:nbn:de:0030-drops-62315},
  doi =		{10.4230/LIPIcs.ICALP.2016.96},
  annote =	{Keywords: Automata, mso, infinite trees, probabilistic temporal logics}
}
Document
Invited Talk
Decidable Extensions of MSO (Invited Talk)

Authors: Mikolaj Bojanczyk

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)


Abstract
This is an overview of the invited talk delivered at the 41st International Symposium on Mathematical Foundations of Computer Science (MFCS-2016).

Cite as

Mikolaj Bojanczyk. Decidable Extensions of MSO (Invited Talk). In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.MFCS.2016.2,
  author =	{Bojanczyk, Mikolaj},
  title =	{{Decidable Extensions of MSO}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.2},
  URN =		{urn:nbn:de:0030-drops-65089},
  doi =		{10.4230/LIPIcs.MFCS.2016.2},
  annote =	{Keywords: monadic second-order logic, extensions, decidability, automata}
}
Document
The MSO+U Theory of (N,<) Is Undecidable

Authors: Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)


Abstract
We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,<) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory.

Cite as

Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk. The MSO+U Theory of (N,<) Is Undecidable. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 21:1-21:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2016.21,
  author =	{Bojanczyk, Mikolaj and Parys, Pawel and Torunczyk, Szymon},
  title =	{{The MSO+U Theory of (N,\langle) Is Undecidable}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{21:1--21:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.21},
  URN =		{urn:nbn:de:0030-drops-57223},
  doi =		{10.4230/LIPIcs.STACS.2016.21},
  annote =	{Keywords: automata, logic, unbounding quantifier, bounds, undecidability}
}
Document
Circuits, Logic and Games (Dagstuhl Seminar 15401)

Authors: Mikolaj Bojanczyk, Meena Mahajan, Thomas Schwentick, and Heribert Vollmer

Published in: Dagstuhl Reports, Volume 5, Issue 9 (2016)


Abstract
Over the years, there has been a lot of interplay between circuit complexity and logic. There are tight connections between small-depth circuit classes and fragments and extensions of firstorder logic, and ideas from games and finite model theory have provided powerful lower bound techniques for circuits. In recent years, there has been an impressive and sustained growth of interest and activity in the intersection of finite model theory and Boolean circuit complexity. The central aim of the seminar was to bring together researchers from these two areas to further strengthen the mutual fertilisation. The seminar focussed on the following specific topics: -The algebraic approach to circuit complexity with its applications to finite model theory -The logic-circuit connection, with a particular emphasis on circuit lower bounds that trigger results in finite model theory like separations between logics - New connections between uniformity conditions on circuit families and logical predicates - Structural complexity and circuit lower bounds inherently using methods from logic and algebra Proof systems with low circuit complexity - Dynamic complexity: understanding the dynamic expressive power of small depth circuit classes The seminar had 43 participants from 11 countries and was very successful with respect to the exchange of recent results, ideas and methodological approaches.

Cite as

Mikolaj Bojanczyk, Meena Mahajan, Thomas Schwentick, and Heribert Vollmer. Circuits, Logic and Games (Dagstuhl Seminar 15401). In Dagstuhl Reports, Volume 5, Issue 9, pp. 105-124, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{bojanczyk_et_al:DagRep.5.9.105,
  author =	{Bojanczyk, Mikolaj and Mahajan, Meena and Schwentick, Thomas and Vollmer, Heribert},
  title =	{{Circuits, Logic and Games (Dagstuhl Seminar 15401)}},
  pages =	{105--124},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{9},
  editor =	{Bojanczyk, Mikolaj and Mahajan, Meena and Schwentick, Thomas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.9.105},
  URN =		{urn:nbn:de:0030-drops-56872},
  doi =		{10.4230/DagRep.5.9.105},
  annote =	{Keywords: computational complexity theory, finite model theory, Boolean circuits, regular languages, finite monoids, Ehrenfeucht-Fraiss\'{e}-games}
}
Document
Nominal Computation Theory (Dagstuhl Seminar 13422)

Authors: Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, and Andrew M. Pitts

Published in: Dagstuhl Reports, Volume 3, Issue 10 (2014)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13422 "Nominal Computation Theory". The underlying theme of the seminar was nominal sets (also known as sets with atoms or Fraenkel-Mostowski sets) and they role and applications in three distinct research areas: automata over infinite alphabets, program semantics using nominal sets and nominal calculi of concurrent processes.

Cite as

Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, and Andrew M. Pitts. Nominal Computation Theory (Dagstuhl Seminar 13422). In Dagstuhl Reports, Volume 3, Issue 10, pp. 58-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@Article{bojanczyk_et_al:DagRep.3.10.58,
  author =	{Bojanczyk, Mikolaj and Klin, Bartek and Kurz, Alexander and Pitts, Andrew M.},
  title =	{{Nominal Computation Theory (Dagstuhl Seminar 13422)}},
  pages =	{58--71},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{10},
  editor =	{Bojanczyk, Mikolaj and Klin, Bartek and Kurz, Alexander and Pitts, Andrew M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.3.10.58},
  URN =		{urn:nbn:de:0030-drops-44285},
  doi =		{10.4230/DagRep.3.10.58},
  annote =	{Keywords: nominal sets, Fraenkel-Mostowski sets}
}
Document
Regular languages of thin trees

Authors: Mikolaj Bojanczyk, Tomasz Idziaszek, and Michal Skrzypczak

Published in: LIPIcs, Volume 20, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)


Abstract
An infinite tree is called thin if it contains only countably many infinite branches. Thin trees can be seen as intermediate structures between infinite words and infinite trees. In this work we investigate properties of regular languages of thin trees. Our main tool is an algebra suitable for thin trees. Using this framework we characterize various classes of regular languages: commutative, open in the standard topology, closed under two variants of bisimulational equivalence, and definable in WMSO logic among all trees. We also show that in various meanings thin trees are not as rich as all infinite trees. In particular we observe a parity index collapse to level (1,3) and a topological complexity collapse to co-analytic sets. Moreover, a gap property is shown: a regular language of thin trees is either WMSO-definable among all trees or co-analytic-complete.

Cite as

Mikolaj Bojanczyk, Tomasz Idziaszek, and Michal Skrzypczak. Regular languages of thin trees. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 20, pp. 562-573, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2013.562,
  author =	{Bojanczyk, Mikolaj and Idziaszek, Tomasz and Skrzypczak, Michal},
  title =	{{Regular languages of thin trees}},
  booktitle =	{30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)},
  pages =	{562--573},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-50-7},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{20},
  editor =	{Portier, Natacha and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2013.562},
  URN =		{urn:nbn:de:0030-drops-39655},
  doi =		{10.4230/LIPIcs.STACS.2013.562},
  annote =	{Keywords: infinite trees, regular languages, effective characterizations, topological complexity}
}
Document
Imperative Programming in Sets with Atoms

Authors: Mikolaj Bojanczyk and Szymon Torunczyk

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)


Abstract
We define an imperative programming language, which extends while programs with a type for storing atoms or hereditarily orbit-finite sets. To deal with an orbit-finite set, the language has a loop construction, which is executed in parallel for all elements of an orbit-finite set. We show examples of programs in this language, e.g. a program for minimising deterministic orbit-finite automata.

Cite as

Mikolaj Bojanczyk and Szymon Torunczyk. Imperative Programming in Sets with Atoms. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 4-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.FSTTCS.2012.4,
  author =	{Bojanczyk, Mikolaj and Torunczyk, Szymon},
  title =	{{Imperative Programming in Sets with Atoms}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{4--15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.4},
  URN =		{urn:nbn:de:0030-drops-38437},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.4},
  annote =	{Keywords: Nominal sets, sets with atoms, while programs}
}
Document
Decidable classes of documents for XPath

Authors: Vince Bárány, Mikolaj Bojanczyk, Diego Figueira, and Pawel Parys

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)


Abstract
We study the satisfiability problem for XPath over XML documents of bounded depth. We define two parameters, called match width and braid width, that assign a number to any class of documents. We show that for all k, satisfiability for XPath restricted to bounded depth documents with match width at most k is decidable; and that XPath is undecidable on any class of documents with unbounded braid width. We conjecture that these two parameters are equivalent, in the sense that a class of documents has bounded match width iff it has bounded braid width.

Cite as

Vince Bárány, Mikolaj Bojanczyk, Diego Figueira, and Pawel Parys. Decidable classes of documents for XPath. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 99-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{barany_et_al:LIPIcs.FSTTCS.2012.99,
  author =	{B\'{a}r\'{a}ny, Vince and Bojanczyk, Mikolaj and Figueira, Diego and Parys, Pawel},
  title =	{{Decidable classes of documents for XPath}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{99--111},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.99},
  URN =		{urn:nbn:de:0030-drops-38512},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.99},
  annote =	{Keywords: XPath, XML, class automata, data trees, data words, satisfiability}
}
Document
Weak MSO+U over infinite trees

Authors: Mikolaj Bojanczyk and Szymon Torunczyk

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)


Abstract
We prove that, over infinite trees, satisfiability is decidable for Weak Monadic Second-Order Logic extended by the unbounding quantifier U. We develop an automaton model, prove that it is effectively equivalent to the logic, and that the automaton model has decidable emptiness.

Cite as

Mikolaj Bojanczyk and Szymon Torunczyk. Weak MSO+U over infinite trees. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 648-660, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2012.648,
  author =	{Bojanczyk, Mikolaj and Torunczyk, Szymon},
  title =	{{Weak MSO+U over infinite trees}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{648--660},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.648},
  URN =		{urn:nbn:de:0030-drops-34279},
  doi =		{10.4230/LIPIcs.STACS.2012.648},
  annote =	{Keywords: Infinite trees, distance automata, MSO+U, profinite words}
}
Document
Data Monoids

Authors: Mikolaj Bojanczyk

Published in: LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)


Abstract
We develop an algebraic theory for languages of data words. We prove that, under certain conditions, a language of data words is definable in first-order logic if and only if its syntactic monoid is aperiodic.

Cite as

Mikolaj Bojanczyk. Data Monoids. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 105-116, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.STACS.2011.105,
  author =	{Bojanczyk, Mikolaj},
  title =	{{Data Monoids}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},
  pages =	{105--116},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Schwentick, Thomas and D\"{u}rr, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.105},
  URN =		{urn:nbn:de:0030-drops-30030},
  doi =		{10.4230/LIPIcs.STACS.2011.105},
  annote =	{Keywords: Monoid, Data Words, Nominal Set, First-Order Logic}
}
Document
Automata for Data Words and Data Trees

Authors: Mikolaj Bojanczyk

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)


Abstract
Data words and data trees appear in verification and XML processing. The term ``data'' means that positions of the word, or tree, are decorated with elements of an infinite set of data values, such as natural numbers or ASCII strings. This talk is a survey of the various automaton models that have been developed for data words and data trees.

Cite as

Mikolaj Bojanczyk. Automata for Data Words and Data Trees. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.RTA.2010.1,
  author =	{Bojanczyk, Mikolaj},
  title =	{{Automata for Data Words and Data Trees}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{1--4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.1},
  URN =		{urn:nbn:de:0030-drops-26397},
  doi =		{10.4230/LIPIcs.RTA.2010.1},
  annote =	{Keywords: Automata, Data Word, Data Tree}
}
Document
Beyond omega-Regular Languages

Authors: Mikolaj Bojanczyk

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)


Abstract
The paper presents some automata and logics on $\omega$-words, which capture all $\omega$-regular languages, and yet still have good closure and decidability properties.

Cite as

Mikolaj Bojanczyk. Beyond omega-Regular Languages. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 11-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.STACS.2010.2440,
  author =	{Bojanczyk, Mikolaj},
  title =	{{Beyond omega-Regular Languages}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{11--16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2440},
  URN =		{urn:nbn:de:0030-drops-24409},
  doi =		{10.4230/LIPIcs.STACS.2010.2440},
  annote =	{Keywords: Automata, monadic second-order logic}
}
Document
Deterministic Automata and Extensions of Weak MSO

Authors: Mikolaj Bojanczyk and Szymon Torunczyk

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)


Abstract
We introduce a new class of automata on infinite words, called min-automata. We prove that min-automata have the same expressive power as weak monadic second-order logic (weak MSO) extended with a new quantifier, the recurrence quantifier. These results are dual to a framework presented in \cite{max-automata}, where max-automata were proved equivalent to weak MSO extended with an unbounding quantifier. We also present a general framework, which tries to explain which types of automata on infinite words correspond to extensions of weak MSO. As another example for the usefulness framework, apart from min- and max-automata, we define an extension of weak MSO with a quantifier that talks about ultimately periodic sets.

Cite as

Mikolaj Bojanczyk and Szymon Torunczyk. Deterministic Automata and Extensions of Weak MSO. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 73-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.FSTTCS.2009.2308,
  author =	{Bojanczyk, Mikolaj and Torunczyk, Szymon},
  title =	{{Deterministic Automata and Extensions of Weak MSO}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{73--84},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2308},
  URN =		{urn:nbn:de:0030-drops-23081},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2308},
  annote =	{Keywords: Deterministic automata, Weak MSO, min-automata, max-automata, BS-automata}
}
Document
Weak MSO with the Unbounding Quantifier

Authors: Mikolaj Bojanczyk

Published in: LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)


Abstract
A new class of languages of infinite words is introduced, called the \emph{max-regular languages}, extending the class of $\omega$-regular languages. The class has two equivalent descriptions: in terms of automata (a type of deterministic counter automaton), and in terms of logic (weak monadic second-order logic with a bounding quantifier). Effective translations between the logic and automata are given.

Cite as

Mikolaj Bojanczyk. Weak MSO with the Unbounding Quantifier. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 159-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{bojanczyk:LIPIcs.STACS.2009.1834,
  author =	{Bojanczyk, Mikolaj},
  title =	{{Weak MSO with the Unbounding Quantifier}},
  booktitle =	{26th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{159--170},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-09-5},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{3},
  editor =	{Albers, Susanne and Marion, Jean-Yves},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1834},
  URN =		{urn:nbn:de:0030-drops-18345},
  doi =		{10.4230/LIPIcs.STACS.2009.1834},
  annote =	{Keywords: Automata, Monadic second-order logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail